; EXPECT: unsat
;; minimized from UFLIA/tokeneer/enclave/progressadminactivity-3.smt2
(set-info :smt-lib-version 2.6)
(set-logic UFLIA)
(set-info :source |
      Tokeneer case study <http://www.adacore.com/home/products/gnatpro/tokeneer/>
  |)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun field.statetype.status () Int)
(declare-fun admin__archivelog () Int)
(declare-fun admin__nullop () Int)
(declare-fun admin__opandnullt__base__first () Int)
(declare-fun admin__opandnullt__base__last () Int)
(declare-fun admin__opandnullt__first () Int)
(declare-fun admin__opandnullt__last () Int)
(declare-fun admin__opandnullt__size () Int)
(declare-fun admin__overridelock () Int)
(declare-fun admin__shutdownop () Int)
(declare-fun admin__updateconfigdata () Int)
(declare-fun alarmtypes__alarming () Int)
(declare-fun alarmtypes__silent () Int)
(declare-fun alarmtypes__statust__base__first () Int)
(declare-fun alarmtypes__statust__base__last () Int)
(declare-fun alarmtypes__statust__first () Int)
(declare-fun alarmtypes__statust__last () Int)
(declare-fun alarmtypes__statust__size () Int)
(declare-fun door__closed () Int)
(declare-fun door__open () Int)
(declare-fun door__t__base__first () Int)
(declare-fun door__t__base__last () Int)
(declare-fun door__t__first () Int)
(declare-fun door__t__last () Int)
(declare-fun door__t__size () Int)
(declare-fun enclavequiescent () Int)
(declare-fun gotadmintoken () Int)
(declare-fun nonquiescentstates__base__first () Int)
(declare-fun nonquiescentstates__base__last () Int)
(declare-fun nonquiescentstates__first () Int)
(declare-fun nonquiescentstates__last () Int)
(declare-fun nonquiescentstates__size () Int)
(declare-fun notenrolled () Int)
(declare-fun privtypes__auditmanager () Int)
(declare-fun privtypes__guard () Int)
(declare-fun privtypes__privileget__base__first () Int)
(declare-fun privtypes__privileget__base__last () Int)
(declare-fun privtypes__privileget__first () Int)
(declare-fun privtypes__privileget__last () Int)
(declare-fun privtypes__privileget__size () Int)
(declare-fun privtypes__securityofficer () Int)
(declare-fun privtypes__useronly () Int)
(declare-fun shutdown () Int)
(declare-fun statust__base__first () Int)
(declare-fun statust__base__last () Int)
(declare-fun statust__first () Int)
(declare-fun statust__last () Int)
(declare-fun statust__size () Int)
(declare-fun waitingendenrol () Int)
(declare-fun waitingenrol () Int)
(declare-fun waitingfinishadminop () Int)
(declare-fun waitingremoveadmintokenfail () Int)
(declare-fun waitingstartadminop () Int)
(declare-fun admintoken__state () Int)
(declare-fun admintoken__state__1 () Int)
(declare-fun init.admintoken__state__1 () Int)
(declare-fun admintoken__state__2 () Int)
(declare-fun init.admintoken__state__2 () Int)
(declare-fun admintoken__state__3 () Int)
(declare-fun init.admintoken__state__3 () Int)
(declare-fun init.admintoken__state () Int)
(declare-fun clock__currenttime () Int)
(declare-fun init.clock__currenttime () Int)
(declare-fun door__state () Int)
(declare-fun door__state__3 () Int)
(declare-fun init.door__state__3 () Int)
(declare-fun init.door__state () Int)
(declare-fun latch__state () Int)
(declare-fun latch__state__3 () Int)
(declare-fun init.latch__state__3 () Int)
(declare-fun init.latch__state () Int)
(declare-fun state () Int)
(declare-fun init.state () Int)
(declare-fun |status'| () Int)
(declare-fun status__1 () Int)
(declare-fun init.status__1 () Int)
(declare-fun status__2 () Int)
(declare-fun init.status__2 () Int)
(declare-fun status__3 () Int)
(declare-fun init.status__3 () Int)
(declare-fun init.status () Int)
(declare-fun theadmin () Int)
(declare-fun theadmin__1 () Int)
(declare-fun init.theadmin__1 () Int)
(declare-fun theadmin__3 () Int)
(declare-fun init.theadmin__3 () Int)
(declare-fun init.theadmin () Int)
(declare-fun admin__opandnullt__pos (Int) Int)
(declare-fun admin__opandnullt__pred (Int) Int)
(declare-fun admin__opandnullt__succ (Int) Int)
(declare-fun admin__opandnullt__val (Int) Int)
(declare-fun admin__prf_rolepresent (Int) Int)
(declare-fun admin__thecurrentop (Int) Int)
(declare-fun admintoken__theauthcertrole (Int) Int)
(declare-fun alarmtypes__statust__pos (Int) Int)
(declare-fun alarmtypes__statust__pred (Int) Int)
(declare-fun alarmtypes__statust__succ (Int) Int)
(declare-fun alarmtypes__statust__val (Int) Int)
(declare-fun bit__and (Int Int) Int)
(declare-fun bit__not (Int Int) Int)
(declare-fun bit__or (Int Int) Int)
(declare-fun bit__xor (Int Int) Int)
(declare-fun character__pos (Int) Int)
(declare-fun character__val (Int) Int)
(declare-fun clock__thecurrenttime (Int) Int)
(declare-fun door__prf_alarmtimeout (Int) Int)
(declare-fun door__t__pos (Int) Int)
(declare-fun door__t__pred (Int) Int)
(declare-fun door__t__succ (Int) Int)
(declare-fun door__t__val (Int) Int)
(declare-fun door__thecurrentdoor (Int) Int)
(declare-fun door__thedooralarm (Int) Int)
(declare-fun integer__pred (Int) Int)
(declare-fun integer__succ (Int) Int)
(declare-fun privtypes__privileget__pos (Int) Int)
(declare-fun privtypes__privileget__pred (Int) Int)
(declare-fun privtypes__privileget__succ (Int) Int)
(declare-fun privtypes__privileget__val (Int) Int)
(declare-fun round__ (Int) Int)
(declare-fun statust__pos (Int) Int)
(declare-fun statust__pred (Int) Int)
(declare-fun statust__succ (Int) Int)
(declare-fun statust__val (Int) Int)
(declare-fun i.div (Int Int) Int)
(declare-fun i.mod (Int Int) Int)
(declare-fun i.mult (Int Int) Int)
(declare-fun i.exp (Int Int) Int)
(declare-fun tm.true () Int)
(declare-fun tm.false () Int)
(declare-fun tm.not (Int) Int)
(declare-fun tm.and (Int Int) Int)
(declare-fun tm.or (Int Int) Int)
(declare-fun tm.iff (Int Int) Int)
(declare-fun tm.eq (Int Int) Int)
(declare-fun tm.ne (Int Int) Int)
(declare-fun tm.lt (Int Int) Int)
(declare-fun tm.le (Int Int) Int)
(declare-fun tuple.2 (Int Int) Int)
(declare-fun a.store (Int Int Int) Int)
(declare-fun a.select (Int Int) Int)
(declare-fun a.mk_const_array (Int) Int)
(declare-fun a.default_array () Int)
(declare-fun r.default_record () Int)
(declare-fun admin__isdoingop (Int) Bool)
(declare-fun admin__ispresent (Int) Bool)
(declare-fun admin__opandnullt__LE (Int Int) Bool)
(declare-fun admin__opandnullt__LT (Int Int) Bool)
(declare-fun admintoken__prf_authcertvalid (Int) Bool)
(declare-fun admintoken__prf_isgood (Int) Bool)
(declare-fun alarmtypes__statust__LE (Int Int) Bool)
(declare-fun alarmtypes__statust__LT (Int Int) Bool)
(declare-fun clock__greaterthanorequal (Int Int) Bool)
(declare-fun currentadminactivitypossible (Int Int) Bool)
(declare-fun door__t__LE (Int Int) Bool)
(declare-fun door__t__LT (Int Int) Bool)
(declare-fun enclave__currentadminactivitypossible (Int Int) Bool)
(declare-fun enclave__enrolmentisinprogress (Int) Bool)
(declare-fun enrolmentisinprogress (Int) Bool)
(declare-fun latch__islocked (Int) Bool)
(declare-fun prf_statusisenclavequiescent (Int) Bool)
(declare-fun prf_statusisgotadmintoken (Int) Bool)
(declare-fun prf_statusisshutdown (Int) Bool)
(declare-fun prf_statusiswaitingfinishadminop (Int) Bool)
(declare-fun prf_statusiswaitingremoveadmintokenfail (Int) Bool)
(declare-fun prf_statusiswaitingstartadminop (Int) Bool)
(declare-fun privtypes__privileget__LE (Int Int) Bool)
(declare-fun privtypes__privileget__LT (Int Int) Bool)
(declare-fun statust__LE (Int Int) Bool)
(declare-fun statust__LT (Int Int) Bool)
(assert (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)))
(assert (=> (not (admin__ispresent theadmin)) (not (admin__isdoingop theadmin))))
(assert (=> (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)) (and (admin__ispresent theadmin) (admin__isdoingop theadmin))))
(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__shutdownop)) (= |status'| waitingstartadminop)))
(assert (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))))
(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__overridelock)) (= (admin__prf_rolepresent theadmin) privtypes__guard)))
(assert (let ((?v_0 (admin__isdoingop theadmin))) (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (or (and ?v_0 (= (admin__thecurrentop theadmin) admin__overridelock)) (not ?v_0)))))
(assert (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)))
(assert (let ((?v_1 (admin__isdoingop theadmin)) (?v_0 (= |status'| waitingstartadminop)) (?v_2 (admin__thecurrentop theadmin)) (?v_3 (= (admin__prf_rolepresent theadmin) privtypes__guard))) (let ((?v_4 (and ?v_1 (= ?v_2 admin__overridelock)))) (not (and (or ?v_0 (= |status'| waitingfinishadminop)) (=> (and ?v_1 (= ?v_2 admin__shutdownop)) ?v_0) (admin__ispresent theadmin) ?v_1 (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)) (=> ?v_3 (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))) (=> ?v_4 ?v_3) (=> ?v_3 (or ?v_4 (not ?v_1))))))))
(check-sat)
(exit)
